Nuprl Definition : existse-ge
11,40
postcript
pdf
existse-ge(
es
;
e
;
e'
.
P
(
e'
)) ==
e'
:es-E(
es
). (es-le(
es
;
e
;
e'
)
P
(
e'
))
latex
Definitions
x
:
A
.
B
(
x
)
,
es-E(
es
)
,
P
Q
,
es-le(
es
;
e
;
e'
)
FDL editor aliases
existse-ge
origin
e':es-E(es). (es-le(es; e; e') 
P(e')) e':es-E(es). (es-le(es; e; e') P(e')) x:A. B(x) Q